(1
 (
  ("(var3 stable)" 0 41)
  ("(var3 up)" 41 77)
  ("(var3 stable)" 77 320)
  ("(var4 stable)" 0 46)
  ("(var4 up)" 46 70)
  ("(var4 stable)" 70 72)
  ("(var4 up)" 72 79)
  ("(var4 stable)" 79 182)
  ("(var4 down)" 182 287)
  ("(var4 stable)" 287 320)
  ("(var1 stable)" 0 48)
  ("(var1 up)" 48 67)
  ("(var1 stable)" 67 320)
  ("(var2 stable)" 0 57)
  ("(var2 up)" 57 59)
  ("(var2 down)" 59 64)
  ("(var2 stable)" 64 110)
  ("(var2 up)" 110 176)
  ("(var2 down)" 176 178)
  ("(var2 up)" 178 202)
  ("(var2 stable)" 202 320)
 )
)
(2
 (
  ("(var3 stable)" 0 67)
  ("(var3 up)" 67 100)
  ("(var3 stable)" 100 313)
  ("(var4 stable)" 0 72)
  ("(var4 up)" 72 97)
  ("(var4 stable)" 97 189)
  ("(var4 down)" 189 276)
  ("(var4 stable)" 276 313)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 95)
  ("(var1 stable)" 95 313)
  ("(var2 stable)" 0 85)
  ("(var2 down)" 85 90)
  ("(var2 up)" 90 205)
  ("(var2 stable)" 205 313)
 )
)
(3
 (
  ("(var3 stable)" 0 78)
  ("(var3 up)" 78 104)
  ("(var3 stable)" 104 343)
  ("(var4 stable)" 0 78)
  ("(var4 up)" 78 103)
  ("(var4 stable)" 103 229)
  ("(var4 down)" 229 231)
  ("(var4 stable)" 231 233)
  ("(var4 down)" 233 308)
  ("(var4 stable)" 308 343)
  ("(var1 stable)" 0 80)
  ("(var1 up)" 80 101)
  ("(var1 stable)" 101 343)
  ("(var2 stable)" 0 89)
  ("(var2 up)" 89 91)
  ("(var2 down)" 91 96)
  ("(var2 up)" 96 212)
  ("(var2 down)" 212 214)
  ("(var2 up)" 214 236)
  ("(var2 stable)" 236 343)
 )
)
(4
 (
  ("(var3 stable)" 0 74)
  ("(var3 up)" 74 80)
  ("(var3 stable)" 80 82)
  ("(var3 up)" 82 101)
  ("(var3 stable)" 101 367)
  ("(var4 stable)" 0 68)
  ("(var4 up)" 68 70)
  ("(var4 stable)" 70 72)
  ("(var4 up)" 72 115)
  ("(var4 stable)" 115 251)
  ("(var4 down)" 251 365)
  ("(var4 up)" 365 367)
  ("(var1 stable)" 0 69)
  ("(var1 up)" 69 71)
  ("(var1 down)" 71 73)
  ("(var1 up)" 73 104)
  ("(var1 down)" 104 107)
  ("(var1 stable)" 107 367)
  ("(var2 stable)" 0 92)
  ("(var2 up)" 92 94)
  ("(var2 down)" 94 99)
  ("(var2 stable)" 99 152)
  ("(var2 up)" 152 226)
  ("(var2 down)" 226 228)
  ("(var2 up)" 228 232)
  ("(var2 stable)" 232 236)
  ("(var2 up)" 236 241)
  ("(var2 stable)" 241 361)
  ("(var2 down)" 361 365)
  ("(var2 up)" 365 367)
 )
)
(5
 (
  ("(var3 stable)" 0 82)
  ("(var3 up)" 82 85)
  ("(var3 stable)" 85 89)
  ("(var3 up)" 89 115)
  ("(var3 stable)" 115 340)
  ("(var4 stable)" 0 84)
  ("(var4 up)" 84 86)
  ("(var4 down)" 86 88)
  ("(var4 up)" 88 116)
  ("(var4 stable)" 116 215)
  ("(var4 down)" 215 325)
  ("(var4 stable)" 325 340)
  ("(var1 stable)" 0 84)
  ("(var1 up)" 84 108)
  ("(var1 stable)" 108 340)
  ("(var2 stable)" 0 100)
  ("(var2 up)" 100 102)
  ("(var2 down)" 102 106)
  ("(var2 stable)" 106 146)
  ("(var2 up)" 146 234)
  ("(var2 stable)" 234 340)
 )
)
(6
 (
  ("(var3 stable)" 0 70)
  ("(var3 up)" 70 100)
  ("(var3 stable)" 100 347)
  ("(var4 stable)" 0 71)
  ("(var4 up)" 71 108)
  ("(var4 down)" 108 110)
  ("(var4 up)" 110 112)
  ("(var4 stable)" 112 231)
  ("(var4 down)" 231 302)
  ("(var4 stable)" 302 347)
  ("(var1 stable)" 0 74)
  ("(var1 up)" 74 100)
  ("(var1 down)" 100 102)
  ("(var1 up)" 102 104)
  ("(var1 stable)" 104 347)
  ("(var2 stable)" 0 88)
  ("(var2 up)" 88 90)
  ("(var2 down)" 90 95)
  ("(var2 stable)" 95 139)
  ("(var2 up)" 139 230)
  ("(var2 stable)" 230 347)
 )
)
(7
 (
  ("(var3 stable)" 0 89)
  ("(var3 down)" 89 91)
  ("(var3 up)" 91 122)
  ("(var3 stable)" 122 378)
  ("(var4 stable)" 0 90)
  ("(var4 up)" 90 122)
  ("(var4 stable)" 122 226)
  ("(var4 down)" 226 228)
  ("(var4 stable)" 228 249)
  ("(var4 down)" 249 330)
  ("(var4 stable)" 330 378)
  ("(var1 stable)" 0 88)
  ("(var1 up)" 88 113)
  ("(var1 down)" 113 115)
  ("(var1 up)" 115 117)
  ("(var1 stable)" 117 378)
  ("(var2 stable)" 0 105)
  ("(var2 up)" 105 107)
  ("(var2 down)" 107 116)
  ("(var2 up)" 116 170)
  ("(var2 stable)" 170 172)
  ("(var2 up)" 172 206)
  ("(var2 stable)" 206 208)
  ("(var2 up)" 208 250)
  ("(var2 stable)" 250 378)
 )
)
(8
 (
  ("(var3 stable)" 0 35)
  ("(var3 up)" 35 64)
  ("(var3 stable)" 64 298)
  ("(var4 stable)" 0 32)
  ("(var4 up)" 32 63)
  ("(var4 stable)" 63 67)
  ("(var4 up)" 67 71)
  ("(var4 stable)" 71 182)
  ("(var4 down)" 182 256)
  ("(var4 stable)" 256 298)
  ("(var1 stable)" 0 34)
  ("(var1 up)" 34 38)
  ("(var1 down)" 38 40)
  ("(var1 up)" 40 59)
  ("(var1 stable)" 59 298)
  ("(var2 stable)" 0 48)
  ("(var2 up)" 48 50)
  ("(var2 down)" 50 55)
  ("(var2 stable)" 55 98)
  ("(var2 up)" 98 185)
  ("(var2 stable)" 185 298)
 )
)
(9
 (
  ("(var3 stable)" 0 76)
  ("(var3 up)" 76 104)
  ("(var3 stable)" 104 317)
  ("(var4 stable)" 0 73)
  ("(var4 up)" 73 104)
  ("(var4 stable)" 104 189)
  ("(var4 down)" 189 273)
  ("(var4 up)" 273 276)
  ("(var4 down)" 276 284)
  ("(var4 stable)" 284 317)
  ("(var1 stable)" 0 78)
  ("(var1 up)" 78 106)
  ("(var1 stable)" 106 317)
  ("(var2 stable)" 0 88)
  ("(var2 up)" 88 92)
  ("(var2 down)" 92 94)
  ("(var2 up)" 94 205)
  ("(var2 stable)" 205 317)
 )
)
(10
 (
  ("(var3 stable)" 0 66)
  ("(var3 up)" 66 69)
  ("(var3 stable)" 69 73)
  ("(var3 up)" 73 77)
  ("(var3 stable)" 77 79)
  ("(var3 up)" 79 102)
  ("(var3 stable)" 102 344)
  ("(var4 stable)" 0 67)
  ("(var4 up)" 67 71)
  ("(var4 down)" 71 73)
  ("(var4 up)" 73 109)
  ("(var4 stable)" 109 205)
  ("(var4 down)" 205 239)
  ("(var4 up)" 239 241)
  ("(var4 down)" 241 303)
  ("(var4 stable)" 303 344)
  ("(var1 stable)" 0 75)
  ("(var1 up)" 75 100)
  ("(var1 stable)" 100 344)
  ("(var2 stable)" 0 87)
  ("(var2 up)" 87 89)
  ("(var2 down)" 89 94)
  ("(var2 up)" 94 218)
  ("(var2 stable)" 218 344)
 )
)
(11
 (
  ("(var3 stable)" 0 58)
  ("(var3 up)" 58 64)
  ("(var3 stable)" 64 66)
  ("(var3 up)" 66 85)
  ("(var3 stable)" 85 87)
  ("(var3 up)" 87 90)
  ("(var3 stable)" 90 341)
  ("(var4 stable)" 0 59)
  ("(var4 up)" 59 94)
  ("(var4 stable)" 94 223)
  ("(var4 down)" 223 292)
  ("(var4 stable)" 292 341)
  ("(var1 stable)" 0 56)
  ("(var1 up)" 56 85)
  ("(var1 down)" 85 87)
  ("(var1 stable)" 87 341)
  ("(var2 stable)" 0 75)
  ("(var2 up)" 75 77)
  ("(var2 down)" 77 82)
  ("(var2 up)" 82 187)
  ("(var2 stable)" 187 192)
  ("(var2 up)" 192 221)
  ("(var2 stable)" 221 341)
 )
)
(12
 (
  ("(var3 stable)" 0 70)
  ("(var3 up)" 70 100)
  ("(var3 stable)" 100 346)
  ("(var4 down)" 0 2)
  ("(var4 stable)" 2 69)
  ("(var4 up)" 69 106)
  ("(var4 stable)" 106 201)
  ("(var4 down)" 201 296)
  ("(var4 stable)" 296 346)
  ("(var1 stable)" 0 70)
  ("(var1 up)" 70 97)
  ("(var1 stable)" 97 346)
  ("(var2 stable)" 0 85)
  ("(var2 up)" 85 87)
  ("(var2 down)" 87 92)
  ("(var2 up)" 92 227)
  ("(var2 stable)" 227 346)
 )
)
(13
 (
  ("(var3 stable)" 0 70)
  ("(var3 up)" 70 96)
  ("(var3 stable)" 96 340)
  ("(var4 stable)" 0 68)
  ("(var4 up)" 68 95)
  ("(var4 down)" 95 97)
  ("(var4 up)" 97 99)
  ("(var4 stable)" 99 200)
  ("(var4 up)" 200 202)
  ("(var4 down)" 202 293)
  ("(var4 stable)" 293 340)
  ("(var1 stable)" 0 69)
  ("(var1 up)" 69 92)
  ("(var1 stable)" 92 340)
  ("(var2 stable)" 0 81)
  ("(var2 up)" 81 83)
  ("(var2 down)" 83 88)
  ("(var2 up)" 88 215)
  ("(var2 down)" 215 218)
  ("(var2 stable)" 218 340)
 )
)
(14
 (
  ("(var3 stable)" 0 84)
  ("(var3 up)" 84 124)
  ("(var3 stable)" 124 349)
  ("(var4 stable)" 0 89)
  ("(var4 up)" 89 126)
  ("(var4 stable)" 126 206)
  ("(var4 down)" 206 336)
  ("(var4 stable)" 336 347)
  ("(var4 down)" 347 349)
  ("(var1 stable)" 0 93)
  ("(var1 up)" 93 112)
  ("(var1 stable)" 112 349)
  ("(var2 stable)" 0 103)
  ("(var2 up)" 103 107)
  ("(var2 down)" 107 109)
  ("(var2 up)" 109 205)
  ("(var2 stable)" 205 208)
  ("(var2 up)" 208 235)
  ("(var2 stable)" 235 349)
 )
)
(15
 (
  ("(var3 stable)" 0 77)
  ("(var3 up)" 77 111)
  ("(var3 stable)" 111 348)
  ("(var4 stable)" 0 70)
  ("(var4 up)" 70 119)
  ("(var4 stable)" 119 213)
  ("(var4 down)" 213 215)
  ("(var4 up)" 215 217)
  ("(var4 down)" 217 320)
  ("(var4 stable)" 320 348)
  ("(var1 stable)" 0 79)
  ("(var1 up)" 79 107)
  ("(var1 stable)" 107 348)
  ("(var2 stable)" 0 92)
  ("(var2 up)" 92 94)
  ("(var2 down)" 94 99)
  ("(var2 up)" 99 233)
  ("(var2 stable)" 233 348)
 )
)
(16
 (
  ("(var3 stable)" 0 49)
  ("(var3 up)" 49 78)
  ("(var3 down)" 78 80)
  ("(var3 stable)" 80 315)
  ("(var4 stable)" 0 49)
  ("(var4 up)" 49 87)
  ("(var4 stable)" 87 173)
  ("(var4 down)" 173 175)
  ("(var4 up)" 175 177)
  ("(var4 down)" 177 268)
  ("(var4 stable)" 268 315)
  ("(var1 stable)" 0 51)
  ("(var1 up)" 51 53)
  ("(var1 stable)" 53 55)
  ("(var1 up)" 55 73)
  ("(var1 stable)" 73 315)
  ("(var2 stable)" 0 63)
  ("(var2 up)" 63 65)
  ("(var2 down)" 65 70)
  ("(var2 up)" 70 180)
  ("(var2 stable)" 180 315)
 )
)
(17
 (
  ("(var3 stable)" 0 36)
  ("(var3 up)" 36 64)
  ("(var3 stable)" 64 319)
  ("(var4 stable)" 0 33)
  ("(var4 up)" 33 76)
  ("(var4 stable)" 76 161)
  ("(var4 down)" 161 204)
  ("(var4 up)" 204 206)
  ("(var4 down)" 206 267)
  ("(var4 stable)" 267 319)
  ("(var1 stable)" 0 34)
  ("(var1 up)" 34 65)
  ("(var1 stable)" 65 319)
  ("(var2 stable)" 0 52)
  ("(var2 up)" 52 55)
  ("(var2 down)" 55 59)
  ("(var2 up)" 59 199)
  ("(var2 stable)" 199 319)
 )
)
(18
 (
  ("(var3 stable)" 0 83)
  ("(var3 up)" 83 111)
  ("(var3 stable)" 111 367)
  ("(var4 stable)" 0 70)
  ("(var4 up)" 70 72)
  ("(var4 stable)" 72 81)
  ("(var4 up)" 81 106)
  ("(var4 stable)" 106 108)
  ("(var4 up)" 108 111)
  ("(var4 down)" 111 113)
  ("(var4 stable)" 113 244)
  ("(var4 down)" 244 332)
  ("(var4 stable)" 332 367)
  ("(var1 stable)" 0 70)
  ("(var1 up)" 70 72)
  ("(var1 down)" 72 74)
  ("(var1 up)" 74 105)
  ("(var1 stable)" 105 367)
  ("(var2 stable)" 0 94)
  ("(var2 up)" 94 96)
  ("(var2 down)" 96 101)
  ("(var2 stable)" 101 143)
  ("(var2 up)" 143 252)
  ("(var2 down)" 252 254)
  ("(var2 up)" 254 256)
  ("(var2 stable)" 256 367)
 )
)
(19
 (
  ("(var3 stable)" 0 59)
  ("(var3 up)" 59 95)
  ("(var3 stable)" 95 341)
  ("(var4 stable)" 0 66)
  ("(var4 up)" 66 103)
  ("(var4 stable)" 103 192)
  ("(var4 down)" 192 194)
  ("(var4 up)" 194 196)
  ("(var4 down)" 196 295)
  ("(var4 stable)" 295 341)
  ("(var1 stable)" 0 66)
  ("(var1 up)" 66 84)
  ("(var1 stable)" 84 87)
  ("(var1 up)" 87 93)
  ("(var1 stable)" 93 341)
  ("(var2 stable)" 0 79)
  ("(var2 up)" 79 83)
  ("(var2 down)" 83 88)
  ("(var2 stable)" 88 130)
  ("(var2 up)" 130 132)
  ("(var2 stable)" 132 135)
  ("(var2 up)" 135 215)
  ("(var2 stable)" 215 341)
 )
)
(20
 (
  ("(var3 stable)" 0 73)
  ("(var3 up)" 73 75)
  ("(var3 down)" 75 78)
  ("(var3 up)" 78 119)
  ("(var3 stable)" 119 358)
  ("(var4 stable)" 0 79)
  ("(var4 up)" 79 81)
  ("(var4 stable)" 81 83)
  ("(var4 up)" 83 114)
  ("(var4 stable)" 114 209)
  ("(var4 down)" 209 308)
  ("(var4 stable)" 308 313)
  ("(var4 down)" 313 315)
  ("(var4 stable)" 315 358)
  ("(var1 stable)" 0 74)
  ("(var1 up)" 74 116)
  ("(var1 stable)" 116 358)
  ("(var2 stable)" 0 96)
  ("(var2 up)" 96 98)
  ("(var2 down)" 98 103)
  ("(var2 up)" 103 246)
  ("(var2 stable)" 246 358)
 )
)
(21
 (
  ("(var3 stable)" 0 80)
  ("(var3 up)" 80 110)
  ("(var3 stable)" 110 335)
  ("(var4 stable)" 0 80)
  ("(var4 up)" 80 82)
  ("(var4 stable)" 82 85)
  ("(var4 up)" 85 111)
  ("(var4 stable)" 111 219)
  ("(var4 down)" 219 298)
  ("(var4 stable)" 298 335)
  ("(var1 stable)" 0 79)
  ("(var1 up)" 79 108)
  ("(var1 stable)" 108 335)
  ("(var2 stable)" 0 96)
  ("(var2 up)" 96 98)
  ("(var2 down)" 98 103)
  ("(var2 up)" 103 218)
  ("(var2 stable)" 218 335)
 )
)
(22
 (
  ("(var3 stable)" 0 71)
  ("(var3 up)" 71 100)
  ("(var3 stable)" 100 340)
  ("(var4 stable)" 0 69)
  ("(var4 down)" 69 71)
  ("(var4 up)" 71 99)
  ("(var4 stable)" 99 202)
  ("(var4 up)" 202 204)
  ("(var4 down)" 204 300)
  ("(var4 stable)" 300 340)
  ("(var1 stable)" 0 74)
  ("(var1 up)" 74 98)
  ("(var1 stable)" 98 338)
  ("(var1 down)" 338 340)
  ("(var2 stable)" 0 84)
  ("(var2 up)" 84 86)
  ("(var2 down)" 86 91)
  ("(var2 up)" 91 219)
  ("(var2 stable)" 219 340)
 )
)
(23
 (
  ("(var3 stable)" 0 46)
  ("(var3 up)" 46 85)
  ("(var3 stable)" 85 311)
  ("(var4 stable)" 0 48)
  ("(var4 up)" 48 80)
  ("(var4 stable)" 80 188)
  ("(var4 down)" 188 273)
  ("(var4 stable)" 273 305)
  ("(var4 up)" 305 309)
  ("(var4 down)" 309 311)
  ("(var1 stable)" 0 50)
  ("(var1 down)" 50 52)
  ("(var1 up)" 52 78)
  ("(var1 stable)" 78 311)
  ("(var2 stable)" 0 62)
  ("(var2 up)" 62 64)
  ("(var2 down)" 64 69)
  ("(var2 up)" 69 201)
  ("(var2 stable)" 201 311)
 )
)
(24
 (
  ("(var3 down)" 0 4)
  ("(var3 up)" 4 7)
  ("(var3 down)" 7 9)
  ("(var3 stable)" 9 38)
  ("(var3 up)" 38 66)
  ("(var3 stable)" 66 290)
  ("(var4 stable)" 0 34)
  ("(var4 up)" 34 68)
  ("(var4 down)" 68 70)
  ("(var4 up)" 70 72)
  ("(var4 stable)" 72 154)
  ("(var4 down)" 154 156)
  ("(var4 up)" 156 158)
  ("(var4 down)" 158 258)
  ("(var4 stable)" 258 290)
  ("(var1 stable)" 0 29)
  ("(var1 up)" 29 62)
  ("(var1 stable)" 62 290)
  ("(var2 stable)" 0 51)
  ("(var2 up)" 51 55)
  ("(var2 down)" 55 57)
  ("(var2 stable)" 57 100)
  ("(var2 up)" 100 159)
  ("(var2 stable)" 159 290)
 )
)
(25
 (
  ("(var3 stable)" 0 70)
  ("(var3 up)" 70 104)
  ("(var3 stable)" 104 347)
  ("(var4 stable)" 0 68)
  ("(var4 up)" 68 70)
  ("(var4 stable)" 70 72)
  ("(var4 up)" 72 113)
  ("(var4 stable)" 113 203)
  ("(var4 down)" 203 206)
  ("(var4 up)" 206 208)
  ("(var4 down)" 208 322)
  ("(var4 up)" 322 324)
  ("(var4 down)" 324 326)
  ("(var4 stable)" 326 347)
  ("(var1 stable)" 0 75)
  ("(var1 up)" 75 101)
  ("(var1 stable)" 101 347)
  ("(var2 stable)" 0 88)
  ("(var2 up)" 88 90)
  ("(var2 down)" 90 95)
  ("(var2 stable)" 95 135)
  ("(var2 up)" 135 209)
  ("(var2 stable)" 209 347)
 )
)
(26
 (
  ("(var3 stable)" 0 36)
  ("(var3 up)" 36 63)
  ("(var3 stable)" 63 284)
  ("(var4 stable)" 0 39)
  ("(var4 up)" 39 68)
  ("(var4 stable)" 68 70)
  ("(var4 up)" 70 72)
  ("(var4 stable)" 72 173)
  ("(var4 down)" 173 245)
  ("(var4 stable)" 245 284)
  ("(var1 stable)" 0 32)
  ("(var1 up)" 32 65)
  ("(var1 stable)" 65 284)
  ("(var2 stable)" 0 49)
  ("(var2 up)" 49 51)
  ("(var2 down)" 51 55)
  ("(var2 up)" 55 170)
  ("(var2 down)" 170 172)
  ("(var2 stable)" 172 284)
 )
)
(27
 (
  ("(var3 stable)" 0 88)
  ("(var3 up)" 88 92)
  ("(var3 down)" 92 94)
  ("(var3 up)" 94 121)
  ("(var3 stable)" 121 369)
  ("(var4 stable)" 0 91)
  ("(var4 up)" 91 129)
  ("(var4 stable)" 129 228)
  ("(var4 down)" 228 333)
  ("(var4 stable)" 333 369)
  ("(var1 stable)" 0 86)
  ("(var1 up)" 86 88)
  ("(var1 down)" 88 90)
  ("(var1 up)" 90 118)
  ("(var1 stable)" 118 369)
  ("(var2 stable)" 0 106)
  ("(var2 up)" 106 108)
  ("(var2 down)" 108 113)
  ("(var2 up)" 113 217)
  ("(var2 stable)" 217 220)
  ("(var2 up)" 220 252)
  ("(var2 stable)" 252 369)
 )
)
(28
 (
  ("(var3 stable)" 0 81)
  ("(var3 up)" 81 110)
  ("(var3 stable)" 110 355)
  ("(var4 stable)" 0 79)
  ("(var4 up)" 79 81)
  ("(var4 down)" 81 83)
  ("(var4 up)" 83 90)
  ("(var4 stable)" 90 92)
  ("(var4 up)" 92 113)
  ("(var4 stable)" 113 224)
  ("(var4 down)" 224 335)
  ("(var4 stable)" 335 355)
  ("(var1 stable)" 0 85)
  ("(var1 up)" 85 115)
  ("(var1 stable)" 115 355)
  ("(var2 stable)" 0 96)
  ("(var2 up)" 96 100)
  ("(var2 down)" 100 104)
  ("(var2 stable)" 104 152)
  ("(var2 up)" 152 229)
  ("(var2 stable)" 229 355)
 )
)
(29
 (
  ("(var3 stable)" 0 45)
  ("(var3 up)" 45 75)
  ("(var3 stable)" 75 294)
  ("(var4 stable)" 0 42)
  ("(var4 up)" 42 77)
  ("(var4 stable)" 77 168)
  ("(var4 down)" 168 254)
  ("(var4 stable)" 254 294)
  ("(var1 stable)" 0 44)
  ("(var1 up)" 44 70)
  ("(var1 stable)" 70 294)
  ("(var2 stable)" 0 59)
  ("(var2 up)" 59 61)
  ("(var2 down)" 61 66)
  ("(var2 up)" 66 179)
  ("(var2 stable)" 179 294)
 )
)
(30
 (
  ("(var3 stable)" 0 38)
  ("(var3 up)" 38 68)
  ("(var3 stable)" 68 301)
  ("(var4 stable)" 0 41)
  ("(var4 up)" 41 43)
  ("(var4 stable)" 43 45)
  ("(var4 up)" 45 70)
  ("(var4 stable)" 70 174)
  ("(var4 down)" 174 278)
  ("(var4 stable)" 278 301)
  ("(var1 stable)" 0 48)
  ("(var1 up)" 48 68)
  ("(var1 stable)" 68 301)
  ("(var2 stable)" 0 59)
  ("(var2 up)" 59 61)
  ("(var2 down)" 61 65)
  ("(var2 up)" 65 193)
  ("(var2 down)" 193 195)
  ("(var2 up)" 195 197)
  ("(var2 stable)" 197 301)
 )
)
(31
 (
  ("(var3 stable)" 0 43)
  ("(var3 up)" 43 85)
  ("(var3 stable)" 85 292)
  ("(var4 stable)" 0 45)
  ("(var4 up)" 45 82)
  ("(var4 stable)" 82 164)
  ("(var4 down)" 164 251)
  ("(var4 stable)" 251 292)
  ("(var1 down)" 0 2)
  ("(var1 stable)" 2 46)
  ("(var1 up)" 46 70)
  ("(var1 stable)" 70 292)
  ("(var2 stable)" 0 61)
  ("(var2 up)" 61 63)
  ("(var2 down)" 63 66)
  ("(var2 up)" 66 226)
  ("(var2 stable)" 226 292)
 )
)
(32
 (
  ("(var3 stable)" 0 48)
  ("(var3 up)" 48 93)
  ("(var3 stable)" 93 305)
  ("(var4 stable)" 0 55)
  ("(var4 up)" 55 92)
  ("(var4 stable)" 92 200)
  ("(var4 down)" 200 303)
  ("(var4 stable)" 303 305)
  ("(var1 stable)" 0 59)
  ("(var1 up)" 59 85)
  ("(var1 stable)" 85 305)
  ("(var2 stable)" 0 72)
  ("(var2 up)" 72 74)
  ("(var2 down)" 74 79)
  ("(var2 up)" 79 202)
  ("(var2 stable)" 202 305)
 )
)
(33
 (
  ("(var3 stable)" 0 57)
  ("(var3 up)" 57 85)
  ("(var3 stable)" 85 320)
  ("(var4 stable)" 0 55)
  ("(var4 up)" 55 87)
  ("(var4 down)" 87 89)
  ("(var4 stable)" 89 176)
  ("(var4 down)" 176 178)
  ("(var4 stable)" 178 180)
  ("(var4 down)" 180 303)
  ("(var4 stable)" 303 320)
  ("(var1 down)" 0 2)
  ("(var1 stable)" 2 55)
  ("(var1 up)" 55 86)
  ("(var1 down)" 86 88)
  ("(var1 stable)" 88 320)
  ("(var2 stable)" 0 71)
  ("(var2 up)" 71 73)
  ("(var2 down)" 73 78)
  ("(var2 stable)" 78 121)
  ("(var2 up)" 121 208)
  ("(var2 stable)" 208 320)
 )
)
(34
 (
  ("(var3 stable)" 0 45)
  ("(var3 up)" 45 47)
  ("(var3 down)" 47 49)
  ("(var3 up)" 49 77)
  ("(var3 stable)" 77 320)
  ("(var4 stable)" 0 47)
  ("(var4 up)" 47 82)
  ("(var4 stable)" 82 201)
  ("(var4 down)" 201 280)
  ("(var4 stable)" 280 320)
  ("(var1 stable)" 0 46)
  ("(var1 up)" 46 73)
  ("(var1 stable)" 73 320)
  ("(var2 stable)" 0 62)
  ("(var2 up)" 62 64)
  ("(var2 down)" 64 69)
  ("(var2 up)" 69 181)
  ("(var2 stable)" 181 320)
 )
)
(35
 (
  ("(var3 stable)" 0 74)
  ("(var3 down)" 74 76)
  ("(var3 up)" 76 108)
  ("(var3 stable)" 108 351)
  ("(var4 stable)" 0 73)
  ("(var4 up)" 73 105)
  ("(var4 down)" 105 107)
  ("(var4 up)" 107 110)
  ("(var4 down)" 110 113)
  ("(var4 stable)" 113 213)
  ("(var4 down)" 213 305)
  ("(var4 stable)" 305 351)
  ("(var1 down)" 0 2)
  ("(var1 stable)" 2 74)
  ("(var1 up)" 74 103)
  ("(var1 stable)" 103 351)
  ("(var2 stable)" 0 89)
  ("(var2 up)" 89 93)
  ("(var2 down)" 93 98)
  ("(var2 up)" 98 230)
  ("(var2 stable)" 230 351)
 )
)
(36
 (
  ("(var3 stable)" 0 33)
  ("(var3 up)" 33 58)
  ("(var3 stable)" 58 282)
  ("(var4 stable)" 0 28)
  ("(var4 up)" 28 60)
  ("(var4 stable)" 60 146)
  ("(var4 down)" 146 237)
  ("(var4 stable)" 237 282)
  ("(var1 stable)" 0 31)
  ("(var1 up)" 31 61)
  ("(var1 stable)" 61 282)
  ("(var2 stable)" 0 46)
  ("(var2 up)" 46 48)
  ("(var2 down)" 48 52)
  ("(var2 up)" 52 180)
  ("(var2 stable)" 180 282)
 )
)
(37
 (
  ("(var3 stable)" 0 33)
  ("(var3 up)" 33 62)
  ("(var3 stable)" 62 278)
  ("(var4 stable)" 0 30)
  ("(var4 up)" 30 64)
  ("(var4 stable)" 64 137)
  ("(var4 down)" 137 265)
  ("(var4 stable)" 265 278)
  ("(var1 stable)" 0 28)
  ("(var1 up)" 28 57)
  ("(var1 stable)" 57 278)
  ("(var2 stable)" 0 46)
  ("(var2 up)" 46 48)
  ("(var2 down)" 48 53)
  ("(var2 up)" 53 141)
  ("(var2 down)" 141 143)
  ("(var2 up)" 143 176)
  ("(var2 stable)" 176 278)
 )
)
(38
 (
  ("(var3 stable)" 0 63)
  ("(var3 up)" 63 94)
  ("(var3 stable)" 94 344)
  ("(var4 stable)" 0 57)
  ("(var4 up)" 57 59)
  ("(var4 stable)" 59 61)
  ("(var4 up)" 61 96)
  ("(var4 stable)" 96 212)
  ("(var4 down)" 212 327)
  ("(var4 stable)" 327 344)
  ("(var1 stable)" 0 63)
  ("(var1 up)" 63 95)
  ("(var1 stable)" 95 344)
  ("(var2 stable)" 0 78)
  ("(var2 up)" 78 80)
  ("(var2 down)" 80 85)
  ("(var2 stable)" 85 132)
  ("(var2 up)" 132 228)
  ("(var2 stable)" 228 344)
 )
)
(39
 (
  ("(var3 stable)" 0 29)
  ("(var3 up)" 29 60)
  ("(var3 stable)" 60 62)
  ("(var3 up)" 62 64)
  ("(var3 stable)" 64 288)
  ("(var4 stable)" 0 28)
  ("(var4 up)" 28 66)
  ("(var4 stable)" 66 179)
  ("(var4 down)" 179 245)
  ("(var4 stable)" 245 288)
  ("(var1 stable)" 0 35)
  ("(var1 up)" 35 63)
  ("(var1 stable)" 63 288)
  ("(var2 stable)" 0 47)
  ("(var2 up)" 47 49)
  ("(var2 down)" 49 54)
  ("(var2 up)" 54 181)
  ("(var2 stable)" 181 288)
 )
)
(40
 (
  ("(var3 stable)" 0 43)
  ("(var3 up)" 43 71)
  ("(var3 stable)" 71 319)
  ("(var4 stable)" 0 39)
  ("(var4 up)" 39 76)
  ("(var4 stable)" 76 167)
  ("(var4 down)" 167 208)
  ("(var4 up)" 208 210)
  ("(var4 down)" 210 275)
  ("(var4 stable)" 275 319)
  ("(var1 stable)" 0 42)
  ("(var1 up)" 42 70)
  ("(var1 stable)" 70 319)
  ("(var2 stable)" 0 57)
  ("(var2 up)" 57 61)
  ("(var2 down)" 61 65)
  ("(var2 up)" 65 176)
  ("(var2 stable)" 176 319)
 )
)
(41
 (
  ("(var3 stable)" 0 60)
  ("(var3 up)" 60 85)
  ("(var3 stable)" 85 306)
  ("(var4 stable)" 0 59)
  ("(var4 up)" 59 89)
  ("(var4 stable)" 89 183)
  ("(var4 down)" 183 263)
  ("(var4 stable)" 263 306)
  ("(var1 stable)" 0 55)
  ("(var1 up)" 55 58)
  ("(var1 down)" 58 60)
  ("(var1 up)" 60 81)
  ("(var1 stable)" 81 306)
  ("(var2 stable)" 0 70)
  ("(var2 up)" 70 72)
  ("(var2 down)" 72 77)
  ("(var2 up)" 77 201)
  ("(var2 stable)" 201 306)
 )
)
(42
 (
  ("(var3 stable)" 0 99)
  ("(var3 up)" 99 130)
  ("(var3 stable)" 130 379)
  ("(var4 up)" 0 3)
  ("(var4 down)" 3 5)
  ("(var4 stable)" 5 96)
  ("(var4 up)" 96 129)
  ("(var4 stable)" 129 263)
  ("(var4 down)" 263 265)
  ("(var4 stable)" 265 267)
  ("(var4 down)" 267 339)
  ("(var4 stable)" 339 379)
  ("(var1 stable)" 0 96)
  ("(var1 up)" 96 140)
  ("(var1 stable)" 140 379)
  ("(var2 stable)" 0 113)
  ("(var2 up)" 113 117)
  ("(var2 down)" 117 120)
  ("(var2 up)" 120 283)
  ("(var2 stable)" 283 379)
 )
)
(43
 (
  ("(var3 stable)" 0 46)
  ("(var3 down)" 46 48)
  ("(var3 up)" 48 92)
  ("(var3 stable)" 92 339)
  ("(var4 stable)" 0 59)
  ("(var4 up)" 59 81)
  ("(var4 stable)" 81 83)
  ("(var4 up)" 83 93)
  ("(var4 down)" 93 95)
  ("(var4 up)" 95 97)
  ("(var4 stable)" 97 187)
  ("(var4 up)" 187 190)
  ("(var4 down)" 190 192)
  ("(var4 up)" 192 194)
  ("(var4 down)" 194 196)
  ("(var4 up)" 196 198)
  ("(var4 down)" 198 233)
  ("(var4 up)" 233 235)
  ("(var4 down)" 235 308)
  ("(var4 up)" 308 310)
  ("(var4 down)" 310 312)
  ("(var4 stable)" 312 339)
  ("(var1 stable)" 0 53)
  ("(var1 up)" 53 55)
  ("(var1 down)" 55 57)
  ("(var1 up)" 57 86)
  ("(var1 stable)" 86 339)
  ("(var2 stable)" 0 72)
  ("(var2 up)" 72 74)
  ("(var2 down)" 74 79)
  ("(var2 up)" 79 192)
  ("(var2 down)" 192 194)
  ("(var2 up)" 194 202)
  ("(var2 stable)" 202 339)
 )
)
(44
 (
  ("(var3 stable)" 0 35)
  ("(var3 up)" 35 37)
  ("(var3 stable)" 37 39)
  ("(var3 up)" 39 67)
  ("(var3 stable)" 67 303)
  ("(var4 down)" 0 3)
  ("(var4 stable)" 3 39)
  ("(var4 up)" 39 65)
  ("(var4 stable)" 65 67)
  ("(var4 up)" 67 72)
  ("(var4 down)" 72 74)
  ("(var4 up)" 74 76)
  ("(var4 stable)" 76 188)
  ("(var4 down)" 188 254)
  ("(var4 stable)" 254 300)
  ("(var4 down)" 300 303)
  ("(var1 stable)" 0 39)
  ("(var1 up)" 39 63)
  ("(var1 stable)" 63 303)
  ("(var2 down)" 0 2)
  ("(var2 stable)" 2 53)
  ("(var2 up)" 53 55)
  ("(var2 down)" 55 60)
  ("(var2 up)" 60 188)
  ("(var2 stable)" 188 303)
 )
)
(45
 (
  ("(var3 stable)" 0 49)
  ("(var3 up)" 49 74)
  ("(var3 stable)" 74 291)
  ("(var4 stable)" 0 42)
  ("(var4 up)" 42 77)
  ("(var4 stable)" 77 155)
  ("(var4 down)" 155 255)
  ("(var4 stable)" 255 291)
  ("(var1 stable)" 0 44)
  ("(var1 up)" 44 70)
  ("(var1 stable)" 70 291)
  ("(var2 stable)" 0 57)
  ("(var2 up)" 57 59)
  ("(var2 down)" 59 64)
  ("(var2 up)" 64 177)
  ("(var2 stable)" 177 291)
 )
)
(46
 (
  ("(var3 stable)" 0 73)
  ("(var3 up)" 73 76)
  ("(var3 down)" 76 78)
  ("(var3 up)" 78 103)
  ("(var3 stable)" 103 338)
  ("(var4 stable)" 0 75)
  ("(var4 up)" 75 104)
  ("(var4 stable)" 104 195)
  ("(var4 down)" 195 294)
  ("(var4 stable)" 294 297)
  ("(var4 down)" 297 299)
  ("(var4 stable)" 299 338)
  ("(var1 stable)" 0 79)
  ("(var1 up)" 79 100)
  ("(var1 stable)" 100 338)
  ("(var2 stable)" 0 88)
  ("(var2 up)" 88 90)
  ("(var2 down)" 90 95)
  ("(var2 up)" 95 227)
  ("(var2 stable)" 227 338)
 )
)
(47
 (
  ("(var3 stable)" 0 37)
  ("(var3 up)" 37 65)
  ("(var3 stable)" 65 289)
  ("(var4 stable)" 0 28)
  ("(var4 up)" 28 73)
  ("(var4 stable)" 73 183)
  ("(var4 down)" 183 256)
  ("(var4 stable)" 256 289)
  ("(var1 stable)" 0 32)
  ("(var1 up)" 32 56)
  ("(var1 stable)" 56 59)
  ("(var1 up)" 59 63)
  ("(var1 stable)" 63 289)
  ("(var2 stable)" 0 48)
  ("(var2 up)" 48 50)
  ("(var2 down)" 50 55)
  ("(var2 up)" 55 177)
  ("(var2 stable)" 177 289)
 )
)
(48
 (
  ("(var3 stable)" 0 70)
  ("(var3 up)" 70 105)
  ("(var3 stable)" 105 361)
  ("(var4 stable)" 0 78)
  ("(var4 up)" 78 111)
  ("(var4 down)" 111 113)
  ("(var4 up)" 113 116)
  ("(var4 stable)" 116 221)
  ("(var4 down)" 221 314)
  ("(var4 stable)" 314 316)
  ("(var4 down)" 316 319)
  ("(var4 stable)" 319 361)
  ("(var1 stable)" 0 80)
  ("(var1 up)" 80 82)
  ("(var1 down)" 82 84)
  ("(var1 up)" 84 103)
  ("(var1 stable)" 103 361)
  ("(var2 stable)" 0 93)
  ("(var2 up)" 93 95)
  ("(var2 down)" 95 100)
  ("(var2 up)" 100 208)
  ("(var2 stable)" 208 225)
  ("(var2 up)" 225 227)
  ("(var2 stable)" 227 356)
  ("(var2 down)" 356 358)
  ("(var2 stable)" 358 361)
 )
)
(49
 (
  ("(var3 down)" 0 2)
  ("(var3 stable)" 2 66)
  ("(var3 up)" 66 91)
  ("(var3 stable)" 91 93)
  ("(var3 up)" 93 97)
  ("(var3 stable)" 97 333)
  ("(var4 stable)" 0 60)
  ("(var4 up)" 60 96)
  ("(var4 stable)" 96 214)
  ("(var4 down)" 214 308)
  ("(var4 up)" 308 310)
  ("(var4 down)" 310 312)
  ("(var4 stable)" 312 333)
  ("(var1 stable)" 0 65)
  ("(var1 down)" 65 68)
  ("(var1 up)" 68 73)
  ("(var1 down)" 73 75)
  ("(var1 up)" 75 91)
  ("(var1 stable)" 91 333)
  ("(var2 stable)" 0 80)
  ("(var2 up)" 80 82)
  ("(var2 down)" 82 87)
  ("(var2 up)" 87 213)
  ("(var2 down)" 213 216)
  ("(var2 stable)" 216 333)
 )
)
(50
 (
  ("(var3 stable)" 0 30)
  ("(var3 up)" 30 32)
  ("(var3 down)" 32 35)
  ("(var3 up)" 35 66)
  ("(var3 stable)" 66 289)
  ("(var4 down)" 0 2)
  ("(var4 stable)" 2 38)
  ("(var4 up)" 38 67)
  ("(var4 stable)" 67 156)
  ("(var4 down)" 156 250)
  ("(var4 stable)" 250 253)
  ("(var4 down)" 253 255)
  ("(var4 stable)" 255 289)
  ("(var1 stable)" 0 28)
  ("(var1 up)" 28 66)
  ("(var1 stable)" 66 289)
  ("(var2 stable)" 0 50)
  ("(var2 up)" 50 54)
  ("(var2 down)" 54 56)
  ("(var2 up)" 56 146)
  ("(var2 down)" 146 149)
  ("(var2 up)" 149 184)
  ("(var2 stable)" 184 289)
 )
)
(51
 (
  ("(var3 stable)" 0 78)
  ("(var3 up)" 78 81)
  ("(var3 down)" 81 83)
  ("(var3 up)" 83 109)
  ("(var3 stable)" 109 354)
  ("(var4 stable)" 0 75)
  ("(var4 up)" 75 109)
  ("(var4 stable)" 109 212)
  ("(var4 down)" 212 308)
  ("(var4 stable)" 308 354)
  ("(var1 stable)" 0 77)
  ("(var1 up)" 77 104)
  ("(var1 stable)" 104 354)
  ("(var2 stable)" 0 93)
  ("(var2 up)" 93 95)
  ("(var2 down)" 95 100)
  ("(var2 up)" 100 205)
  ("(var2 down)" 205 207)
  ("(var2 up)" 207 247)
  ("(var2 stable)" 247 354)
 )
)
(52
 (
  ("(var3 stable)" 0 56)
  ("(var3 up)" 56 80)
  ("(var3 stable)" 80 325)
  ("(var4 stable)" 0 52)
  ("(var4 up)" 52 81)
  ("(var4 stable)" 81 176)
  ("(var4 down)" 176 281)
  ("(var4 up)" 281 284)
  ("(var4 stable)" 284 325)
  ("(var1 stable)" 0 52)
  ("(var1 up)" 52 79)
  ("(var1 stable)" 79 325)
  ("(var2 stable)" 0 66)
  ("(var2 up)" 66 70)
  ("(var2 down)" 70 74)
  ("(var2 up)" 74 215)
  ("(var2 stable)" 215 325)
 )
)
(53
 (
  ("(var3 stable)" 0 2)
  ("(var3 down)" 2 4)
  ("(var3 up)" 4 6)
  ("(var3 stable)" 6 59)
  ("(var3 up)" 59 96)
  ("(var3 stable)" 96 323)
  ("(var4 stable)" 0 68)
  ("(var4 up)" 68 95)
  ("(var4 down)" 95 97)
  ("(var4 stable)" 97 184)
  ("(var4 down)" 184 274)
  ("(var4 stable)" 274 323)
  ("(var1 stable)" 0 68)
  ("(var1 up)" 68 90)
  ("(var1 stable)" 90 323)
  ("(var2 stable)" 0 77)
  ("(var2 up)" 77 79)
  ("(var2 down)" 79 84)
  ("(var2 stable)" 84 124)
  ("(var2 up)" 124 206)
  ("(var2 stable)" 206 323)
 )
)
(54
 (
  ("(var3 stable)" 0 41)
  ("(var3 up)" 41 66)
  ("(var3 stable)" 66 296)
  ("(var4 stable)" 0 40)
  ("(var4 up)" 40 72)
  ("(var4 stable)" 72 186)
  ("(var4 down)" 186 252)
  ("(var4 stable)" 252 296)
  ("(var1 stable)" 0 40)
  ("(var1 up)" 40 68)
  ("(var1 stable)" 68 296)
  ("(var2 stable)" 0 54)
  ("(var2 up)" 54 56)
  ("(var2 down)" 56 61)
  ("(var2 up)" 61 158)
  ("(var2 stable)" 158 296)
 )
)
(55
 (
  ("(var3 stable)" 0 36)
  ("(var3 down)" 36 38)
  ("(var3 up)" 38 40)
  ("(var3 stable)" 40 42)
  ("(var3 up)" 42 70)
  ("(var3 stable)" 70 306)
  ("(var4 stable)" 0 39)
  ("(var4 up)" 39 72)
  ("(var4 stable)" 72 191)
  ("(var4 up)" 191 193)
  ("(var4 down)" 193 261)
  ("(var4 stable)" 261 304)
  ("(var4 up)" 304 306)
  ("(var1 stable)" 0 40)
  ("(var1 up)" 40 44)
  ("(var1 down)" 44 46)
  ("(var1 up)" 46 67)
  ("(var1 stable)" 67 306)
  ("(var2 stable)" 0 55)
  ("(var2 up)" 55 57)
  ("(var2 down)" 57 62)
  ("(var2 stable)" 62 104)
  ("(var2 up)" 104 182)
  ("(var2 down)" 182 184)
  ("(var2 stable)" 184 306)
 )
)
(56
 (
  ("(var3 stable)" 0 61)
  ("(var3 up)" 61 92)
  ("(var3 stable)" 92 332)
  ("(var4 stable)" 0 63)
  ("(var4 up)" 63 96)
  ("(var4 stable)" 96 211)
  ("(var4 down)" 211 290)
  ("(var4 stable)" 290 295)
  ("(var4 down)" 295 297)
  ("(var4 stable)" 297 332)
  ("(var1 stable)" 0 65)
  ("(var1 up)" 65 88)
  ("(var1 stable)" 88 332)
  ("(var2 stable)" 0 76)
  ("(var2 up)" 76 78)
  ("(var2 down)" 78 83)
  ("(var2 up)" 83 218)
  ("(var2 stable)" 218 332)
 )
)
(57
 (
  ("(var3 stable)" 0 91)
  ("(var3 up)" 91 125)
  ("(var3 stable)" 125 371)
  ("(var4 stable)" 0 85)
  ("(var4 up)" 85 123)
  ("(var4 stable)" 123 256)
  ("(var4 down)" 256 355)
  ("(var4 stable)" 355 369)
  ("(var4 up)" 369 371)
  ("(var1 stable)" 0 91)
  ("(var1 up)" 91 111)
  ("(var1 stable)" 111 113)
  ("(var1 up)" 113 117)
  ("(var1 down)" 117 120)
  ("(var1 up)" 120 122)
  ("(var1 stable)" 122 371)
  ("(var2 stable)" 0 105)
  ("(var2 up)" 105 109)
  ("(var2 down)" 109 113)
  ("(var2 up)" 113 274)
  ("(var2 stable)" 274 371)
 )
)
(58
 (
  ("(var3 stable)" 0 36)
  ("(var3 up)" 36 72)
  ("(var3 stable)" 72 308)
  ("(var4 stable)" 0 41)
  ("(var4 up)" 41 71)
  ("(var4 stable)" 71 174)
  ("(var4 down)" 174 261)
  ("(var4 stable)" 261 308)
  ("(var1 stable)" 0 47)
  ("(var1 down)" 47 49)
  ("(var1 up)" 49 70)
  ("(var1 stable)" 70 308)
  ("(var2 stable)" 0 57)
  ("(var2 up)" 57 59)
  ("(var2 down)" 59 64)
  ("(var2 up)" 64 169)
  ("(var2 down)" 169 171)
  ("(var2 stable)" 171 308)
 )
)
(59
 (
  ("(var3 stable)" 0 76)
  ("(var3 up)" 76 104)
  ("(var3 stable)" 104 317)
  ("(var4 stable)" 0 74)
  ("(var4 up)" 74 100)
  ("(var4 stable)" 100 210)
  ("(var4 down)" 210 272)
  ("(var4 stable)" 272 317)
  ("(var1 stable)" 0 76)
  ("(var1 up)" 76 87)
  ("(var1 stable)" 87 89)
  ("(var1 up)" 89 100)
  ("(var1 stable)" 100 317)
  ("(var2 stable)" 0 82)
  ("(var2 up)" 82 86)
  ("(var2 down)" 86 91)
  ("(var2 up)" 91 214)
  ("(var2 stable)" 214 317)
 )
)
(60
 (
  ("(var3 stable)" 0 36)
  ("(var3 up)" 36 40)
  ("(var3 down)" 40 42)
  ("(var3 up)" 42 71)
  ("(var3 stable)" 71 323)
  ("(var4 stable)" 0 42)
  ("(var4 up)" 42 71)
  ("(var4 stable)" 71 75)
  ("(var4 up)" 75 77)
  ("(var4 stable)" 77 179)
  ("(var4 down)" 179 288)
  ("(var4 stable)" 288 323)
  ("(var1 stable)" 0 37)
  ("(var1 up)" 37 50)
  ("(var1 down)" 50 52)
  ("(var1 up)" 52 74)
  ("(var1 stable)" 74 323)
  ("(var2 stable)" 0 56)
  ("(var2 up)" 56 60)
  ("(var2 down)" 60 64)
  ("(var2 up)" 64 116)
  ("(var2 stable)" 116 118)
  ("(var2 up)" 118 120)
  ("(var2 stable)" 120 122)
  ("(var2 up)" 122 191)
  ("(var2 stable)" 191 323)
 )
)
(61
 (
  ("(var3 stable)" 0 34)
  ("(var3 up)" 34 58)
  ("(var3 stable)" 58 279)
  ("(var4 stable)" 0 35)
  ("(var4 up)" 35 63)
  ("(var4 stable)" 63 151)
  ("(var4 down)" 151 228)
  ("(var4 stable)" 228 231)
  ("(var4 down)" 231 239)
  ("(var4 stable)" 239 277)
  ("(var4 up)" 277 279)
  ("(var1 stable)" 0 35)
  ("(var1 up)" 35 59)
  ("(var1 stable)" 59 279)
  ("(var2 stable)" 0 48)
  ("(var2 up)" 48 50)
  ("(var2 down)" 50 55)
  ("(var2 up)" 55 159)
  ("(var2 down)" 159 161)
  ("(var2 up)" 161 164)
  ("(var2 stable)" 164 279)
 )
)
(62
 (
  ("(var3 stable)" 0 88)
  ("(var3 up)" 88 123)
  ("(var3 stable)" 123 371)
  ("(var4 stable)" 0 83)
  ("(var4 up)" 83 123)
  ("(var4 stable)" 123 260)
  ("(var4 down)" 260 333)
  ("(var4 stable)" 333 371)
  ("(var1 down)" 0 2)
  ("(var1 stable)" 2 94)
  ("(var1 up)" 94 125)
  ("(var1 down)" 125 127)
  ("(var1 stable)" 127 371)
  ("(var2 stable)" 0 105)
  ("(var2 up)" 105 109)
  ("(var2 down)" 109 114)
  ("(var2 stable)" 114 161)
  ("(var2 up)" 161 230)
  ("(var2 stable)" 230 371)
 )
)
(63
 (
  ("(var3 stable)" 0 34)
  ("(var3 up)" 34 36)
  ("(var3 stable)" 36 39)
  ("(var3 up)" 39 67)
  ("(var3 stable)" 67 317)
  ("(var4 stable)" 0 41)
  ("(var4 up)" 41 75)
  ("(var4 down)" 75 77)
  ("(var4 stable)" 77 177)
  ("(var4 down)" 177 179)
  ("(var4 up)" 179 181)
  ("(var4 down)" 181 277)
  ("(var4 stable)" 277 317)
  ("(var1 stable)" 0 42)
  ("(var1 up)" 42 67)
  ("(var1 stable)" 67 317)
  ("(var2 stable)" 0 53)
  ("(var2 up)" 53 55)
  ("(var2 down)" 55 60)
  ("(var2 up)" 60 187)
  ("(var2 down)" 187 189)
  ("(var2 up)" 189 191)
  ("(var2 stable)" 191 317)
 )
)
(64
 (
  ("(var3 stable)" 0 34)
  ("(var3 up)" 34 63)
  ("(var3 down)" 63 65)
  ("(var3 up)" 65 68)
  ("(var3 stable)" 68 303)
  ("(var4 stable)" 0 39)
  ("(var4 up)" 39 74)
  ("(var4 stable)" 74 182)
  ("(var4 down)" 182 186)
  ("(var4 up)" 186 188)
  ("(var4 down)" 188 260)
  ("(var4 up)" 260 263)
  ("(var4 down)" 263 265)
  ("(var4 stable)" 265 303)
  ("(var1 stable)" 0 38)
  ("(var1 up)" 38 64)
  ("(var1 down)" 64 66)
  ("(var1 up)" 66 70)
  ("(var1 stable)" 70 303)
  ("(var2 stable)" 0 52)
  ("(var2 up)" 52 54)
  ("(var2 down)" 54 59)
  ("(var2 stable)" 59 98)
  ("(var2 up)" 98 181)
  ("(var2 stable)" 181 303)
 )
)
(65
 (
  ("(var3 stable)" 0 30)
  ("(var3 up)" 30 63)
  ("(var3 stable)" 63 310)
  ("(var4 stable)" 0 33)
  ("(var4 up)" 33 65)
  ("(var4 down)" 65 67)
  ("(var4 up)" 67 70)
  ("(var4 stable)" 70 164)
  ("(var4 down)" 164 261)
  ("(var4 up)" 261 263)
  ("(var4 stable)" 263 310)
  ("(var1 stable)" 0 37)
  ("(var1 up)" 37 39)
  ("(var1 down)" 39 41)
  ("(var1 up)" 41 63)
  ("(var1 stable)" 63 310)
  ("(var2 stable)" 0 50)
  ("(var2 up)" 50 52)
  ("(var2 down)" 52 57)
  ("(var2 stable)" 57 103)
  ("(var2 up)" 103 173)
  ("(var2 stable)" 173 310)
 )
)
(66
 (
  ("(var3 stable)" 0 78)
  ("(var3 up)" 78 111)
  ("(var3 stable)" 111 360)
  ("(var4 stable)" 0 83)
  ("(var4 up)" 83 87)
  ("(var4 stable)" 87 89)
  ("(var4 up)" 89 115)
  ("(var4 stable)" 115 117)
  ("(var4 up)" 117 119)
  ("(var4 stable)" 119 219)
  ("(var4 down)" 219 316)
  ("(var4 stable)" 316 360)
  ("(var1 stable)" 0 83)
  ("(var1 up)" 83 109)
  ("(var1 stable)" 109 360)
  ("(var2 stable)" 0 96)
  ("(var2 up)" 96 100)
  ("(var2 down)" 100 105)
  ("(var2 stable)" 105 150)
  ("(var2 up)" 150 237)
  ("(var2 stable)" 237 360)
 )
)
(67
 (
  ("(var3 stable)" 0 68)
  ("(var3 up)" 68 70)
  ("(var3 down)" 70 72)
  ("(var3 up)" 72 99)
  ("(var3 stable)" 99 355)
  ("(var4 stable)" 0 64)
  ("(var4 up)" 64 104)
  ("(var4 down)" 104 106)
  ("(var4 stable)" 106 210)
  ("(var4 up)" 210 213)
  ("(var4 down)" 213 320)
  ("(var4 up)" 320 323)
  ("(var4 down)" 323 325)
  ("(var4 stable)" 325 355)
  ("(var1 stable)" 0 59)
  ("(var1 up)" 59 61)
  ("(var1 stable)" 61 64)
  ("(var1 up)" 64 82)
  ("(var1 down)" 82 84)
  ("(var1 up)" 84 94)
  ("(var1 stable)" 94 355)
  ("(var2 stable)" 0 82)
  ("(var2 up)" 82 86)
  ("(var2 down)" 86 91)
  ("(var2 stable)" 91 139)
  ("(var2 up)" 139 202)
  ("(var2 down)" 202 204)
  ("(var2 up)" 204 207)
  ("(var2 stable)" 207 353)
  ("(var2 down)" 353 355)
 )
)
(68
 (
  ("(var3 stable)" 0 73)
  ("(var3 up)" 73 104)
  ("(var3 stable)" 104 337)
  ("(var4 stable)" 0 66)
  ("(var4 down)" 66 68)
  ("(var4 up)" 68 110)
  ("(var4 stable)" 110 198)
  ("(var4 up)" 198 200)
  ("(var4 down)" 200 300)
  ("(var4 stable)" 300 337)
  ("(var1 stable)" 0 75)
  ("(var1 down)" 75 78)
  ("(var1 up)" 78 102)
  ("(var1 stable)" 102 337)
  ("(var2 stable)" 0 87)
  ("(var2 up)" 87 89)
  ("(var2 down)" 89 94)
  ("(var2 up)" 94 206)
  ("(var2 stable)" 206 337)
 )
)
(69
 (
  ("(var3 stable)" 0 49)
  ("(var3 down)" 49 51)
  ("(var3 up)" 51 57)
  ("(var3 stable)" 57 59)
  ("(var3 up)" 59 82)
  ("(var3 stable)" 82 84)
  ("(var3 up)" 84 86)
  ("(var3 stable)" 86 337)
  ("(var4 stable)" 0 42)
  ("(var4 down)" 42 44)
  ("(var4 up)" 44 61)
  ("(var4 down)" 61 63)
  ("(var4 up)" 63 77)
  ("(var4 stable)" 77 79)
  ("(var4 up)" 79 93)
  ("(var4 stable)" 93 191)
  ("(var4 down)" 191 285)
  ("(var4 up)" 285 287)
  ("(var4 down)" 287 299)
  ("(var4 stable)" 299 337)
  ("(var1 stable)" 0 52)
  ("(var1 up)" 52 61)
  ("(var1 stable)" 61 63)
  ("(var1 up)" 63 84)
  ("(var1 stable)" 84 337)
  ("(var2 stable)" 0 70)
  ("(var2 up)" 70 72)
  ("(var2 down)" 72 81)
  ("(var2 up)" 81 202)
  ("(var2 stable)" 202 337)
 )
)
(70
 (
  ("(var3 stable)" 0 58)
  ("(var3 up)" 58 60)
  ("(var3 stable)" 60 62)
  ("(var3 up)" 62 92)
  ("(var3 stable)" 92 328)
  ("(var4 stable)" 0 59)
  ("(var4 up)" 59 61)
  ("(var4 stable)" 61 63)
  ("(var4 up)" 63 89)
  ("(var4 stable)" 89 189)
  ("(var4 down)" 189 310)
  ("(var4 stable)" 310 328)
  ("(var1 stable)" 0 60)
  ("(var1 up)" 60 63)
  ("(var1 down)" 63 65)
  ("(var1 up)" 65 88)
  ("(var1 down)" 88 90)
  ("(var1 stable)" 90 328)
  ("(var2 stable)" 0 75)
  ("(var2 up)" 75 77)
  ("(var2 down)" 77 82)
  ("(var2 up)" 82 214)
  ("(var2 down)" 214 216)
  ("(var2 up)" 216 218)
  ("(var2 stable)" 218 328)
 )
)
(71
 (
  ("(var3 stable)" 0 92)
  ("(var3 up)" 92 117)
  ("(var3 stable)" 117 374)
  ("(var4 stable)" 0 94)
  ("(var4 up)" 94 124)
  ("(var4 stable)" 124 220)
  ("(var4 down)" 220 335)
  ("(var4 stable)" 335 374)
  ("(var1 stable)" 0 95)
  ("(var1 up)" 95 127)
  ("(var1 stable)" 127 374)
  ("(var2 stable)" 0 106)
  ("(var2 up)" 106 108)
  ("(var2 down)" 108 113)
  ("(var2 up)" 113 250)
  ("(var2 stable)" 250 374)
 )
)
(72
 (
  ("(var3 stable)" 0 84)
  ("(var3 up)" 84 111)
  ("(var3 stable)" 111 330)
  ("(var4 stable)" 0 81)
  ("(var4 up)" 81 126)
  ("(var4 stable)" 126 207)
  ("(var4 down)" 207 308)
  ("(var4 stable)" 308 330)
  ("(var1 stable)" 0 86)
  ("(var1 up)" 86 111)
  ("(var1 stable)" 111 330)
  ("(var2 stable)" 0 97)
  ("(var2 up)" 97 99)
  ("(var2 down)" 99 106)
  ("(var2 up)" 106 133)
  ("(var2 down)" 133 135)
  ("(var2 up)" 135 137)
  ("(var2 down)" 137 139)
  ("(var2 up)" 139 214)
  ("(var2 down)" 214 216)
  ("(var2 stable)" 216 330)
 )
)
(73
 (
  ("(var3 stable)" 0 54)
  ("(var3 up)" 54 89)
  ("(var3 stable)" 89 313)
  ("(var4 stable)" 0 58)
  ("(var4 up)" 58 93)
  ("(var4 down)" 93 95)
  ("(var4 stable)" 95 177)
  ("(var4 down)" 177 269)
  ("(var4 stable)" 269 313)
  ("(var1 stable)" 0 60)
  ("(var1 up)" 60 85)
  ("(var1 stable)" 85 313)
  ("(var2 stable)" 0 74)
  ("(var2 up)" 74 76)
  ("(var2 down)" 76 81)
  ("(var2 up)" 81 136)
  ("(var2 stable)" 136 138)
  ("(var2 up)" 138 209)
  ("(var2 stable)" 209 313)
 )
)
(74
 (
  ("(var3 stable)" 0 74)
  ("(var3 up)" 74 105)
  ("(var3 stable)" 105 107)
  ("(var3 up)" 107 109)
  ("(var3 stable)" 109 359)
  ("(var4 stable)" 0 77)
  ("(var4 up)" 77 120)
  ("(var4 stable)" 120 211)
  ("(var4 up)" 211 213)
  ("(var4 down)" 213 320)
  ("(var4 stable)" 320 359)
  ("(var1 stable)" 0 78)
  ("(var1 up)" 78 110)
  ("(var1 stable)" 110 359)
  ("(var2 stable)" 0 94)
  ("(var2 up)" 94 98)
  ("(var2 down)" 98 102)
  ("(var2 stable)" 102 145)
  ("(var2 up)" 145 151)
  ("(var2 stable)" 151 153)
  ("(var2 up)" 153 196)
  ("(var2 down)" 196 198)
  ("(var2 up)" 198 222)
  ("(var2 stable)" 222 359)
 )
)
(75
 (
  ("(var3 stable)" 0 83)
  ("(var3 up)" 83 120)
  ("(var3 stable)" 120 338)
  ("(var4 stable)" 0 84)
  ("(var4 up)" 84 109)
  ("(var4 stable)" 109 111)
  ("(var4 up)" 111 115)
  ("(var4 down)" 115 117)
  ("(var4 up)" 117 121)
  ("(var4 down)" 121 123)
  ("(var4 stable)" 123 209)
  ("(var4 down)" 209 297)
  ("(var4 stable)" 297 338)
  ("(var1 stable)" 0 84)
  ("(var1 up)" 84 117)
  ("(var1 stable)" 117 338)
  ("(var2 stable)" 0 100)
  ("(var2 up)" 100 102)
  ("(var2 down)" 102 107)
  ("(var2 up)" 107 216)
  ("(var2 stable)" 216 338)
 )
)
(76
 (
  ("(var3 stable)" 0 78)
  ("(var3 up)" 78 83)
  ("(var3 down)" 83 85)
  ("(var3 up)" 85 108)
  ("(var3 stable)" 108 355)
  ("(var4 stable)" 0 80)
  ("(var4 up)" 80 82)
  ("(var4 stable)" 82 85)
  ("(var4 up)" 85 106)
  ("(var4 stable)" 106 229)
  ("(var4 down)" 229 313)
  ("(var4 stable)" 313 355)
  ("(var1 stable)" 0 75)
  ("(var1 down)" 75 77)
  ("(var1 up)" 77 80)
  ("(var1 stable)" 80 82)
  ("(var1 up)" 82 109)
  ("(var1 stable)" 109 355)
  ("(var2 stable)" 0 94)
  ("(var2 up)" 94 96)
  ("(var2 down)" 96 101)
  ("(var2 up)" 101 233)
  ("(var2 down)" 233 235)
  ("(var2 up)" 235 237)
  ("(var2 stable)" 237 355)
 )
)
(77
 (
  ("(var3 stable)" 0 67)
  ("(var3 up)" 67 99)
  ("(var3 stable)" 99 320)
  ("(var4 stable)" 0 73)
  ("(var4 up)" 73 101)
  ("(var4 stable)" 101 188)
  ("(var4 down)" 188 287)
  ("(var4 stable)" 287 320)
  ("(var1 stable)" 0 75)
  ("(var1 down)" 75 77)
  ("(var1 up)" 77 95)
  ("(var1 stable)" 95 320)
  ("(var2 stable)" 0 84)
  ("(var2 up)" 84 86)
  ("(var2 down)" 86 91)
  ("(var2 up)" 91 214)
  ("(var2 stable)" 214 320)
 )
)
(78
 (
  ("(var3 stable)" 0 71)
  ("(var3 up)" 71 73)
  ("(var3 down)" 73 75)
  ("(var3 up)" 75 106)
  ("(var3 stable)" 106 335)
  ("(var4 stable)" 0 73)
  ("(var4 up)" 73 110)
  ("(var4 stable)" 110 200)
  ("(var4 down)" 200 303)
  ("(var4 stable)" 303 335)
  ("(var1 stable)" 0 75)
  ("(var1 up)" 75 99)
  ("(var1 stable)" 99 335)
  ("(var2 stable)" 0 88)
  ("(var2 up)" 88 90)
  ("(var2 down)" 90 95)
  ("(var2 up)" 95 191)
  ("(var2 stable)" 191 194)
  ("(var2 up)" 194 227)
  ("(var2 stable)" 227 335)
 )
)
(79
 (
  ("(var3 stable)" 0 44)
  ("(var3 up)" 44 80)
  ("(var3 stable)" 80 324)
  ("(var4 stable)" 0 41)
  ("(var4 up)" 41 74)
  ("(var4 stable)" 74 76)
  ("(var4 up)" 76 78)
  ("(var4 stable)" 78 188)
  ("(var4 up)" 188 190)
  ("(var4 down)" 190 267)
  ("(var4 stable)" 267 324)
  ("(var1 stable)" 0 38)
  ("(var1 up)" 38 70)
  ("(var1 stable)" 70 324)
  ("(var2 stable)" 0 58)
  ("(var2 up)" 58 60)
  ("(var2 down)" 60 65)
  ("(var2 up)" 65 202)
  ("(var2 down)" 202 204)
  ("(var2 up)" 204 206)
  ("(var2 stable)" 206 324)
 )
)
(80
 (
  ("(var3 stable)" 0 79)
  ("(var3 up)" 79 103)
  ("(var3 stable)" 103 327)
  ("(var4 stable)" 0 72)
  ("(var4 up)" 72 107)
  ("(var4 stable)" 107 198)
  ("(var4 down)" 198 200)
  ("(var4 up)" 200 202)
  ("(var4 down)" 202 297)
  ("(var4 stable)" 297 327)
  ("(var1 stable)" 0 75)
  ("(var1 up)" 75 77)
  ("(var1 stable)" 77 80)
  ("(var1 up)" 80 100)
  ("(var1 stable)" 100 327)
  ("(var2 stable)" 0 89)
  ("(var2 up)" 89 91)
  ("(var2 down)" 91 96)
  ("(var2 up)" 96 214)
  ("(var2 stable)" 214 327)
 )
)
(81
 (
  ("(var3 stable)" 0 60)
  ("(var3 up)" 60 90)
  ("(var3 stable)" 90 341)
  ("(var4 stable)" 0 50)
  ("(var4 up)" 50 52)
  ("(var4 down)" 52 54)
  ("(var4 up)" 54 90)
  ("(var4 down)" 90 92)
  ("(var4 up)" 92 94)
  ("(var4 stable)" 94 223)
  ("(var4 down)" 223 297)
  ("(var4 stable)" 297 341)
  ("(var1 stable)" 0 63)
  ("(var1 up)" 63 92)
  ("(var1 stable)" 92 341)
  ("(var2 stable)" 0 74)
  ("(var2 up)" 74 80)
  ("(var2 down)" 80 84)
  ("(var2 stable)" 84 128)
  ("(var2 up)" 128 194)
  ("(var2 stable)" 194 341)
 )
)
(82
 (
  ("(var3 down)" 0 2)
  ("(var3 stable)" 2 43)
  ("(var3 up)" 43 79)
  ("(var3 down)" 79 81)
  ("(var3 up)" 81 84)
  ("(var3 stable)" 84 322)
  ("(var4 stable)" 0 43)
  ("(var4 down)" 43 45)
  ("(var4 up)" 45 86)
  ("(var4 down)" 86 88)
  ("(var4 up)" 88 90)
  ("(var4 stable)" 90 206)
  ("(var4 down)" 206 274)
  ("(var4 stable)" 274 279)
  ("(var4 down)" 279 281)
  ("(var4 stable)" 281 322)
  ("(var1 stable)" 0 40)
  ("(var1 up)" 40 64)
  ("(var1 stable)" 64 66)
  ("(var1 up)" 66 75)
  ("(var1 stable)" 75 322)
  ("(var2 stable)" 0 59)
  ("(var2 up)" 59 61)
  ("(var2 down)" 61 66)
  ("(var2 stable)" 66 111)
  ("(var2 up)" 111 113)
  ("(var2 stable)" 113 115)
  ("(var2 up)" 115 176)
  ("(var2 stable)" 176 322)
 )
)
(83
 (
  ("(var3 stable)" 0 88)
  ("(var3 up)" 88 112)
  ("(var3 stable)" 112 334)
  ("(var4 stable)" 0 87)
  ("(var4 up)" 87 115)
  ("(var4 stable)" 115 218)
  ("(var4 down)" 218 288)
  ("(var4 up)" 288 290)
  ("(var4 down)" 290 298)
  ("(var4 stable)" 298 334)
  ("(var1 stable)" 0 86)
  ("(var1 down)" 86 88)
  ("(var1 up)" 88 112)
  ("(var1 stable)" 112 334)
  ("(var2 stable)" 0 99)
  ("(var2 up)" 99 101)
  ("(var2 down)" 101 106)
  ("(var2 up)" 106 150)
  ("(var2 down)" 150 152)
  ("(var2 up)" 152 225)
  ("(var2 stable)" 225 334)
 )
)
(84
 (
  ("(var3 stable)" 0 53)
  ("(var3 up)" 53 78)
  ("(var3 stable)" 78 305)
  ("(var4 stable)" 0 57)
  ("(var4 up)" 57 85)
  ("(var4 stable)" 85 165)
  ("(var4 down)" 165 271)
  ("(var4 stable)" 271 305)
  ("(var1 stable)" 0 57)
  ("(var1 up)" 57 77)
  ("(var1 stable)" 77 305)
  ("(var2 stable)" 0 66)
  ("(var2 up)" 66 68)
  ("(var2 down)" 68 73)
  ("(var2 stable)" 73 116)
  ("(var2 up)" 116 213)
  ("(var2 stable)" 213 305)
 )
)
(85
 (
  ("(var3 stable)" 0 59)
  ("(var3 up)" 59 93)
  ("(var3 stable)" 93 331)
  ("(var4 stable)" 0 56)
  ("(var4 down)" 56 58)
  ("(var4 up)" 58 93)
  ("(var4 down)" 93 95)
  ("(var4 stable)" 95 201)
  ("(var4 down)" 201 291)
  ("(var4 stable)" 291 331)
  ("(var1 stable)" 0 65)
  ("(var1 up)" 65 85)
  ("(var1 stable)" 85 331)
  ("(var2 stable)" 0 75)
  ("(var2 up)" 75 77)
  ("(var2 down)" 77 82)
  ("(var2 up)" 82 205)
  ("(var2 stable)" 205 331)
 )
)
(86
 (
  ("(var3 stable)" 0 89)
  ("(var3 up)" 89 117)
  ("(var3 stable)" 117 354)
  ("(var4 stable)" 0 87)
  ("(var4 up)" 87 115)
  ("(var4 stable)" 115 154)
  ("(var4 down)" 154 156)
  ("(var4 stable)" 156 158)
  ("(var4 up)" 158 161)
  ("(var4 stable)" 161 228)
  ("(var4 down)" 228 323)
  ("(var4 stable)" 323 354)
  ("(var1 stable)" 0 91)
  ("(var1 up)" 91 115)
  ("(var1 stable)" 115 354)
  ("(var2 stable)" 0 103)
  ("(var2 up)" 103 105)
  ("(var2 down)" 105 110)
  ("(var2 up)" 110 208)
  ("(var2 stable)" 208 212)
  ("(var2 up)" 212 249)
  ("(var2 stable)" 249 354)
 )
)
(87
 (
  ("(var3 stable)" 0 34)
  ("(var3 up)" 34 37)
  ("(var3 stable)" 37 39)
  ("(var3 up)" 39 63)
  ("(var3 stable)" 63 295)
  ("(var4 stable)" 0 32)
  ("(var4 up)" 32 65)
  ("(var4 stable)" 65 155)
  ("(var4 down)" 155 249)
  ("(var4 stable)" 249 295)
  ("(var1 stable)" 0 36)
  ("(var1 up)" 36 38)
  ("(var1 stable)" 38 41)
  ("(var1 up)" 41 58)
  ("(var1 stable)" 58 295)
  ("(var2 stable)" 0 50)
  ("(var2 up)" 50 52)
  ("(var2 down)" 52 54)
  ("(var2 up)" 54 226)
  ("(var2 stable)" 226 295)
 )
)
(88
 (
  ("(var3 stable)" 0 81)
  ("(var3 up)" 81 113)
  ("(var3 stable)" 113 342)
  ("(var4 stable)" 0 83)
  ("(var4 up)" 83 88)
  ("(var4 stable)" 88 90)
  ("(var4 up)" 90 113)
  ("(var4 stable)" 113 201)
  ("(var4 down)" 201 302)
  ("(var4 stable)" 302 342)
  ("(var1 stable)" 0 84)
  ("(var1 up)" 84 117)
  ("(var1 stable)" 117 342)
  ("(var2 stable)" 0 98)
  ("(var2 up)" 98 100)
  ("(var2 down)" 100 105)
  ("(var2 up)" 105 232)
  ("(var2 stable)" 232 342)
 )
)
(89
 (
  ("(var3 stable)" 0 60)
  ("(var3 up)" 60 63)
  ("(var3 stable)" 63 67)
  ("(var3 up)" 67 88)
  ("(var3 stable)" 88 325)
  ("(var4 stable)" 0 60)
  ("(var4 up)" 60 100)
  ("(var4 stable)" 100 185)
  ("(var4 down)" 185 278)
  ("(var4 stable)" 278 280)
  ("(var4 up)" 280 282)
  ("(var4 down)" 282 285)
  ("(var4 stable)" 285 325)
  ("(var1 stable)" 0 61)
  ("(var1 up)" 61 89)
  ("(var1 stable)" 89 325)
  ("(var2 stable)" 0 76)
  ("(var2 up)" 76 78)
  ("(var2 down)" 78 83)
  ("(var2 up)" 83 203)
  ("(var2 stable)" 203 325)
 )
)
(90
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 109)
  ("(var3 stable)" 109 362)
  ("(var4 stable)" 0 74)
  ("(var4 up)" 74 76)
  ("(var4 stable)" 76 78)
  ("(var4 up)" 78 106)
  ("(var4 down)" 106 109)
  ("(var4 up)" 109 113)
  ("(var4 stable)" 113 216)
  ("(var4 down)" 216 309)
  ("(var4 stable)" 309 362)
  ("(var1 stable)" 0 79)
  ("(var1 up)" 79 98)
  ("(var1 stable)" 98 362)
  ("(var2 stable)" 0 89)
  ("(var2 up)" 89 92)
  ("(var2 down)" 92 98)
  ("(var2 up)" 98 198)
  ("(var2 stable)" 198 202)
  ("(var2 up)" 202 206)
  ("(var2 stable)" 206 362)
 )
)
(91
 (
  ("(var3 stable)" 0 89)
  ("(var3 up)" 89 111)
  ("(var3 stable)" 111 113)
  ("(var3 up)" 113 116)
  ("(var3 stable)" 116 363)
  ("(var4 stable)" 0 87)
  ("(var4 up)" 87 129)
  ("(var4 stable)" 129 235)
  ("(var4 down)" 235 317)
  ("(var4 stable)" 317 363)
  ("(var1 stable)" 0 90)
  ("(var1 up)" 90 115)
  ("(var1 down)" 115 117)
  ("(var1 stable)" 117 363)
  ("(var2 stable)" 0 103)
  ("(var2 up)" 103 105)
  ("(var2 down)" 105 110)
  ("(var2 stable)" 110 152)
  ("(var2 up)" 152 235)
  ("(var2 stable)" 235 363)
 )
)
(92
 (
  ("(var3 stable)" 0 89)
  ("(var3 up)" 89 92)
  ("(var3 down)" 92 95)
  ("(var3 up)" 95 127)
  ("(var3 down)" 127 129)
  ("(var3 stable)" 129 378)
  ("(var4 stable)" 0 92)
  ("(var4 up)" 92 130)
  ("(var4 down)" 130 132)
  ("(var4 stable)" 132 237)
  ("(var4 up)" 237 239)
  ("(var4 down)" 239 270)
  ("(var4 stable)" 270 272)
  ("(var4 down)" 272 337)
  ("(var4 stable)" 337 378)
  ("(var1 stable)" 0 92)
  ("(var1 up)" 92 94)
  ("(var1 stable)" 94 97)
  ("(var1 up)" 97 127)
  ("(var1 down)" 127 129)
  ("(var1 stable)" 129 378)
  ("(var2 stable)" 0 112)
  ("(var2 up)" 112 116)
  ("(var2 down)" 116 119)
  ("(var2 up)" 119 285)
  ("(var2 down)" 285 287)
  ("(var2 up)" 287 289)
  ("(var2 stable)" 289 378)
 )
)
(93
 (
  ("(var3 stable)" 0 72)
  ("(var3 up)" 72 103)
  ("(var3 stable)" 103 331)
  ("(var4 stable)" 0 68)
  ("(var4 up)" 68 99)
  ("(var4 down)" 99 101)
  ("(var4 stable)" 101 193)
  ("(var4 down)" 193 219)
  ("(var4 up)" 219 221)
  ("(var4 down)" 221 286)
  ("(var4 stable)" 286 331)
  ("(var1 stable)" 0 72)
  ("(var1 up)" 72 99)
  ("(var1 stable)" 99 331)
  ("(var2 stable)" 0 86)
  ("(var2 up)" 86 88)
  ("(var2 down)" 88 93)
  ("(var2 up)" 93 221)
  ("(var2 stable)" 221 331)
 )
)
(94
 (
  ("(var3 stable)" 0 49)
  ("(var3 up)" 49 75)
  ("(var3 down)" 75 77)
  ("(var3 stable)" 77 314)
  ("(var4 stable)" 0 49)
  ("(var4 up)" 49 78)
  ("(var4 stable)" 78 173)
  ("(var4 down)" 173 212)
  ("(var4 up)" 212 214)
  ("(var4 down)" 214 284)
  ("(var4 up)" 284 286)
  ("(var4 down)" 286 288)
  ("(var4 stable)" 288 314)
  ("(var1 stable)" 0 43)
  ("(var1 up)" 43 75)
  ("(var1 stable)" 75 314)
  ("(var2 stable)" 0 62)
  ("(var2 up)" 62 64)
  ("(var2 down)" 64 69)
  ("(var2 stable)" 69 110)
  ("(var2 up)" 110 208)
  ("(var2 stable)" 208 314)
 )
)
(95
 (
  ("(var3 stable)" 0 89)
  ("(var3 up)" 89 119)
  ("(var3 down)" 119 121)
  ("(var3 up)" 121 123)
  ("(var3 stable)" 123 360)
  ("(var4 stable)" 0 87)
  ("(var4 down)" 87 89)
  ("(var4 up)" 89 91)
  ("(var4 stable)" 91 94)
  ("(var4 up)" 94 124)
  ("(var4 stable)" 124 215)
  ("(var4 down)" 215 320)
  ("(var4 stable)" 320 360)
  ("(var1 stable)" 0 94)
  ("(var1 up)" 94 98)
  ("(var1 stable)" 98 100)
  ("(var1 up)" 100 121)
  ("(var1 stable)" 121 360)
  ("(var2 stable)" 0 105)
  ("(var2 up)" 105 107)
  ("(var2 down)" 107 112)
  ("(var2 stable)" 112 154)
  ("(var2 up)" 154 210)
  ("(var2 stable)" 210 212)
  ("(var2 up)" 212 242)
  ("(var2 down)" 242 245)
  ("(var2 up)" 245 249)
  ("(var2 stable)" 249 360)
 )
)
(96
 (
  ("(var3 stable)" 0 71)
  ("(var3 up)" 71 75)
  ("(var3 stable)" 75 77)
  ("(var3 up)" 77 106)
  ("(var3 stable)" 106 334)
  ("(var4 stable)" 0 70)
  ("(var4 up)" 70 103)
  ("(var4 stable)" 103 218)
  ("(var4 down)" 218 220)
  ("(var4 stable)" 220 222)
  ("(var4 down)" 222 286)
  ("(var4 stable)" 286 334)
  ("(var1 stable)" 0 71)
  ("(var1 up)" 71 76)
  ("(var1 stable)" 76 78)
  ("(var1 up)" 78 96)
  ("(var1 stable)" 96 334)
  ("(var2 stable)" 0 86)
  ("(var2 up)" 86 88)
  ("(var2 down)" 88 93)
  ("(var2 stable)" 93 136)
  ("(var2 up)" 136 209)
  ("(var2 stable)" 209 334)
 )
)
(97
 (
  ("(var3 stable)" 0 65)
  ("(var3 up)" 65 105)
  ("(var3 stable)" 105 331)
  ("(var4 stable)" 0 72)
  ("(var4 up)" 72 106)
  ("(var4 stable)" 106 186)
  ("(var4 down)" 186 307)
  ("(var4 stable)" 307 331)
  ("(var1 stable)" 0 79)
  ("(var1 up)" 79 99)
  ("(var1 stable)" 99 331)
  ("(var2 stable)" 0 88)
  ("(var2 up)" 88 90)
  ("(var2 down)" 90 97)
  ("(var2 up)" 97 231)
  ("(var2 stable)" 231 331)
 )
)
(98
 (
  ("(var3 stable)" 0 85)
  ("(var3 up)" 85 114)
  ("(var3 stable)" 114 364)
  ("(var4 stable)" 0 87)
  ("(var4 up)" 87 119)
  ("(var4 stable)" 119 227)
  ("(var4 down)" 227 318)
  ("(var4 stable)" 318 364)
  ("(var1 stable)" 0 86)
  ("(var1 up)" 86 113)
  ("(var1 stable)" 113 364)
  ("(var2 stable)" 0 102)
  ("(var2 up)" 102 104)
  ("(var2 down)" 104 109)
  ("(var2 up)" 109 238)
  ("(var2 down)" 238 240)
  ("(var2 stable)" 240 364)
 )
)
(99
 (
  ("(var3 stable)" 0 36)
  ("(var3 up)" 36 63)
  ("(var3 stable)" 63 280)
  ("(var4 stable)" 0 40)
  ("(var4 up)" 40 67)
  ("(var4 stable)" 67 154)
  ("(var4 down)" 154 238)
  ("(var4 stable)" 238 280)
  ("(var1 stable)" 0 40)
  ("(var1 up)" 40 57)
  ("(var1 stable)" 57 280)
  ("(var2 stable)" 0 47)
  ("(var2 up)" 47 49)
  ("(var2 down)" 49 54)
  ("(var2 stable)" 54 93)
  ("(var2 up)" 93 123)
  ("(var2 down)" 123 125)
  ("(var2 up)" 125 172)
  ("(var2 stable)" 172 280)
 )
)
(100
 (
  ("(var3 stable)" 0 51)
  ("(var3 up)" 51 89)
  ("(var3 stable)" 89 324)
  ("(var4 stable)" 0 51)
  ("(var4 down)" 51 53)
  ("(var4 up)" 53 85)
  ("(var4 stable)" 85 184)
  ("(var4 down)" 184 311)
  ("(var4 up)" 311 314)
  ("(var4 down)" 314 318)
  ("(var4 up)" 318 324)
  ("(var1 stable)" 0 56)
  ("(var1 up)" 56 77)
  ("(var1 down)" 77 79)
  ("(var1 stable)" 79 324)
  ("(var2 stable)" 0 67)
  ("(var2 up)" 67 69)
  ("(var2 down)" 69 74)
  ("(var2 stable)" 74 120)
  ("(var2 up)" 120 206)
  ("(var2 stable)" 206 324)
 )
)
